perm filename PNUELI[S80,JMC] blob sn#506139 filedate 1980-04-26 generic text, type C, neo UTF8
COMMENT āŠ—   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002		Francez and Pnueli (1978) use time as a parameter and the
C00003 ENDMK
CāŠ—;
	Francez and Pnueli (1978) use time as a parameter and the
program counter as a distinguished variable in order to state and
prove facts about programs that don't stop.